\documentclass[11pt,a4paper]{article}
\usepackage{latexsym}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{dsfont}
\usepackage{tikz}
\usetikzlibrary{calc,intersections,angles,quotes}
\usepackage{listings}
\usepackage{ifthen}
\usepackage{paralist}

\parskip        0mm
\oddsidemargin  0in
\evensidemargin 0in
\textwidth      6in
\topmargin      0in
\marginparwidth 30pt
\textheight     9.2in
\headheight     .1in
\headsep        .1mm

\lstset{
  basicstyle=\footnotesize\ttfamily, % Standardschrift
  numberstyle=\tiny,          % Stil der Zeilennummern
  numbersep=5pt,              % Abstand der Nummern zum Text
  tabsize=2,                  % Groesse von Tabs
  extendedchars=true,         %
  breaklines=true,            % Zeilen werden Umgebrochen
  keywordstyle=\ttfamily,
  stringstyle=\ttfamily, % Farbe der String
  showspaces=false,           % Leerzeichen anzeigen ?
  showtabs=false,             % Tabs anzeigen ?
  xleftmargin=17pt,
  framexleftmargin=17pt,
  framexrightmargin=5pt,
  framexbottommargin=4pt,
  showstringspaces=false      % Leerzeichen in Strings anzeigen ?
}
\lstloadlanguages{
  C , C++, ml
}

\title{VU Programm- und Systemverifikation\\
\Large Assignment 1: Assertions, Testing, and Coverage}
\author{Name: name last name\qquad
  Matr. number: 11907086}
\date{Due: April 22, 2021, 1pm}


\newcommand{\entrynode}{
    \begin{tikzpicture}
      \draw (0,0) circle (3pt);
      \draw[->,>=stealth] (-7pt,0)--(-3pt,0);
    \end{tikzpicture}
}

\begin{document}

\maketitle

\section{Coverage Metrics}

Consider the following program fragment and test suite:\\
\noindent
\begin{tabular}{cc}
  \begin{minipage}{.45\textwidth}
    \begin{tabbing}
      \quad\=\quad\=\qquad\=\qquad\=\\\kill
      {\tt unsigned gcd (unsigned x, unsigned y) \{}\\
      \>{\tt unsigned m, k;}\\
      \>{\tt if (x > y) \{}\\
      \>\>{\tt k = x;}\\
      \>\>{\tt m = y;}\\
      \>{\tt \} else \{}\\
      \>\>{\tt k = y;}\\
      \>\>{\tt m = x;}\\
      \>{\tt \}}\\
      \>{\tt while (m != 0) \{}\\
      \>\>{\tt unsigned r = k \% m;}\\
      \>\>{\tt k = m;}\\
      \>\>{\tt m = r;}\\
      \>{\tt \}}\\
      \>{\tt return k;}\\
      {\tt \}}\\
    \end{tabbing}
  \end{minipage} &
  \begin{minipage}{.45\textwidth}
    \begin{tabular}{|c|c||l|}
      \hline
      \multicolumn{2}{|c||}{Inputs} & \multicolumn{1}{|c|}{Outputs}\\
      \hline
      {\tt x} & {\tt y} & return value\\
      \hline
      0 & 0 & 0\\\hline
      0 & 1 & 0\\\hline
      3 & 2 & 1\\\hline
    \end{tabular}
  \end{minipage}
\end{tabular}

\subsection{Control-Flow-Based Coverage Criteria (2.5 points)}

Indicate (\checkmark) 
which of the following coverage criteria are satisfied by 
the test-suite above.
\begin{center}
  \begin{tabular}{|l|l|l|}
    \hline
    & \multicolumn{2}{|c|}{satisfied}\\
    \hline
        {\bf Criterion} & yes & no\\ \hline
    path coverage && \checkmark \\\hline 
    statement coverage & \checkmark &\\\hline 
    branch coverage & \checkmark &\\\hline 
    decision coverage & \checkmark &\\\hline 
  \end{tabular}
\end{center}
For each coverage criterion that is \emph{not} satisfied, explain why
this is the case:

\textit{Path coverage} is not achieved, in particular because our program fragment includes a loop. If we convert the program fragment to an isomorphic graph representation, we can specify paths as sequences of edges. Loop constructs in a C program are essentially loops or at least cycles in our graph representation. Because the loop condition can be true an arbitrary amount of times, path coverage is really only achieved if we cover all loop lengths. But for our specific test-suite, there are many possible paths that include more loop iterations that aren't covered.

As for the other criteria, because of the simplicity of this program fragment, statements, branches and decisions effectively collapse into the same meaning and they are all fulfilled together.
\subsection{Data-Flow-Based Coverage Criteria (4 points)}

Indicate (\checkmark) 
which of the following coverage criteria are satisfied by 
the test-suite above
(here, the parameters of the function do not constitute definitions,
the {\tt return} statement is a c-use):

\begin{center}
  \begin{tabular}{|l|l|l|}
    \hline
    & \multicolumn{2}{|c|}{satisfied}\\
    \hline    
    {\bf Criterion} & yes & no\\ \hline
    all-defs & \checkmark & \\    \hline
    all-c-uses & & \checkmark \\    \hline
    all-p-uses & \checkmark & \\    \hline
    all-c-uses/some-p-uses & & \checkmark \\     \hline
    all-du-paths & & \checkmark \\     \hline
  \end{tabular}
\end{center}

For each coverage criterion that is not satisfied, explain why
this is the case:

\texttt{all-c-uses} is not satisfied because of the loop definitions \texttt{r = k \% m} and \texttt{k = m}. Both constitute a \texttt{c-use} but are only executed if the loop is entered. The first two test cases of our suite prevent us from ever entering the loop, so these \texttt{c-use}s are never executed after the definitions \texttt{k = y} and \texttt{m = x}.

Because \texttt{all-c-uses} is not (even vacuously) satisfied, it follows that \texttt{all-c-uses/some-p-uses} is also not satisfied.

\texttt{all-du-paths} is the strictest coverage criterion out of all of them, so it makes sense to expect this one not to be satisfied either. Because \texttt{all-c-uses} is not satisfied, it follows that this criterion is also not satisfied.

\pagebreak
\subsection{Achieving Full Coverage (1 point)}

  Consider the two coverage criteria below. 
  \begin{compactitem}
  \item If the test-suite from above does not satisfy the
    coverage criterion, augment it with the 
    \emph{minimal} number of test-cases such that this
    criterion is satisfied. If full coverage cannot be achieved, 
    explain why.
  \item If the coverage criterion is
    already achieved, explain why.
  \end{compactitem}
 
\noindent
\begin{center}
  \begin{minipage}{.4\textwidth}\centering
    {\bf all-c-uses}\\[1ex]
    \begin{tabular}{|c|c|l|}
      \hline
      \multicolumn{2}{|c||}{Inputs} & \multicolumn{1}{|c|}{Outputs}\\
      \hline
      {\tt x} & {\tt y} & result\\
      \hline
        2&3&1  \\
      \hline

    \end{tabular}
  \end{minipage} \hfill
  \begin{minipage}{.4\textwidth}\centering
    {\bf all-uses}\\[1ex]
    \begin{tabular}{|c|c|l|}
      \hline
      \multicolumn{2}{|c||}{Inputs} & \multicolumn{1}{|c|}{Outputs}\\
      \hline
      {\tt x} & {\tt y} & result\\
      \hline
        2&3&1  \\
      \hline

    \end{tabular}
  \end{minipage} 
\end{center}

As \texttt{all-p-uses} is already satisfied, to satisfy \texttt{all-uses} we only need to augment our test-suite with the test cases that are necessary to satisfy \texttt{all-c-uses}.

\vfill

\subsection{General Questions (2.5 points)}
\noindent
  Indicate whether the following statements are true or false!\\[2ex]

  \noindent
  \begin{tabular}{p{.65\textwidth}cc}
    {\bf Statement} & {\bf True} & {\bf False}\\[1ex]
    If a test-suite achieves {\tt all-c-uses} and
    {\tt all-defs} coverage, it also achieves
    {\tt all-c-uses/some-p-uses} coverage. & $\bigcirc$ & $\checkmark$\\ 
    &&\\
    If a test-suite achieves path coverage,
    it also achieves statement coverage. & $\checkmark$ & $\bigcirc$\\ 
    &&\\
    If a test-suite does not achieve {\tt all-uses} coverage,
    it cannot achieve {\tt all-c-uses} either. & $\bigcirc$ & $\checkmark$\\ 
    &&\\
    For any given program, it is always possible to achieve
    MC/DC coverage.
    & $\bigcirc$ & $\checkmark$\\ 
    &&\\
    If full statement coverage cannot be achieved, then
    the program contains unreachable code.
    & $\checkmark$ & $\bigcirc$\\ 
  \end{tabular}
\vfill

\newpage
\subsection{Formal Definition (1 point)}

Let $S_{\entrynode}, S_1, \ldots, S_n$ be the sets of reachable
states at program locations $\entrynode, 1, \ldots, n\in V$, respectively.
Morover, given the conditional statement at program location $\ell$,
let $C_{\ell}$ be corresponding decision. Assume that all branches
correspond to conditional statements.

Define an abstraction function $\alpha$ and an abstract domain
such that 
\begin{displaymath}
  \forall i\in V\,.\,\alpha(S_i) = \top
\end{displaymath}
if (and only if) full branch coverage can be reached.

\newcommand\defequals{\mathrel{\stackrel{\makebox[0pt]{\mbox{\normalfont\tiny def}}}{=}}}
\begin{displaymath}
  \alpha(S_i) \defequals
\begin{cases}
  \{ \sigma(C_i) \mid \sigma \in S_i \} ,& \text{if line } i \text{ has condition } C_i \\
  \top & \text{else}
\end{cases}
\end{displaymath}

This is indeed very similar to a definition found in the lecture, the lattice that is formed is also the same:

\newcommand{\smallwedge}{\mathrel{\text{\raisebox{0.25ex}{\scalebox{0.8}{$\wedge$}}}}}
\newcommand{\smallvee}{\mathrel{\text{\raisebox{0.25ex}{\scalebox{0.8}{$\vee$}}}}}

\[
\{ true, false \}
\]
\[
\{ true \} \quad \quad \quad \quad \quad \{ false \}
\]
\[
\emptyset
\]

\newpage
\section{Equivalence Partitioning and Boundary Testing}

\noindent
If you who had contact with a person who has tested
positive for COVID-19, the function {\tt classify} below
will determine whether you had a category I contact,
a category II contact, or neither.

\begin{center}
\begin{tabbing}
  {\tt category classify (}\,\={\tt int time,}\\
  \>{\tt int distance,}\\
  \>{\tt int their\_age,}\\
  \>{\tt int your\_age);}
\end{tabbing}
\end{center}

It uses the following data-types and parameters:
\begin{itemize}
\item {\tt category} is an enum type defined as
  {\tt enum priority \{C1, C2, NEITHER\};}
\item {\tt time} is the (cumulative) amount of time
  (in minutes) of exposure.
\item {\tt distance} is the minimal distance (in meters)
  to the infected person.
\item {\tt their\_age} is the age of the person who
  tested postive for {\tt COVID-19}.
\item {\tt your\_age} is the age of the person that
  is to be classified.
\end{itemize}

The function {\tt classify} is supposed to implement the following
rules:
\begin{itemize}
\item A person who (cumulatively) spent at least 15 minutes
  in less than 2 meters distance from a person older than 10 years
  of age is classified as category I contact.
\item Children younger than 10 years who were in contact
  (for at least 15 minutes in less than 2 meters distance) with
  a child also younger than 10 years that tested positive for COVID-19
  are classified as category II contacts.
\item A person who (cumulatively) spent less than 15 minutes
  with an infected person or kept a distance of at least 2 meters
  does not fall into category I or II.
\end{itemize}

\pagebreak

\subsection{Equivalence Partitioning (2 points)}

From the specification above, derive equivalence classes for the
function {\tt classify}. Use the table below to partition them into
\emph{valid equivalence classes} (valid inputs) and
\emph{invalid equivalence classes} (invalid inputs).
Label each of the equivalence classes clearly with a number
(in the according column).
For each correct \underline{\emph{equivalence class}} you can score
$\frac{1}{2}$ a point (up to 2 points).\\
{\small (Do not provide test-cases here -- that's task 2.2)}\\[1ex]

\subsubsection{Valid Equivalence Classes}

\begin{tabular}{|p{.92\textwidth}|p{.03\textwidth}|}
  \hline
  {\bf Condition} & {\bf ID} \\
  \hline
    \texttt{their\_age > 10 $\land$ time >= 15 $\land$ distance < 2, all >= 0 $\implies$ C1} & 1 \\
  \hline
    \texttt{your\_age <= 10 $\land$ their\_age <= 10 $\land$ time >= 15 $\land$ distance < 2, all >= 0 $\implies$ C2} & 2 \\
  \hline
    \texttt{time < 15, all >= 0 $\implies$ NEITHER} & 3 \\
  \hline
    \texttt{distance >= 2, all >= 0 $\implies$ NEITHER} & 4 \\
  \hline
    \texttt{your\_age > 10 $\land$ their\_age <= 10 $\land$ time >= 15 $\land$ distance < 2, all >= 0 $\implies$ NEITHER} & 5 \\
  \hline
\end{tabular}
\bigskip

Do note that going strictly by the specification, coming in contact with a person that is exactly of age 10 would neither be categorized as a \texttt{C1} or \texttt{C2} contact, because the boundaries are specified using language that hints at exclusive boundaries. Of course in real life this would likely be an error in the specification and something to bring up, but because this is an exercise, I have instead opted for dropping a note here and making the (hopefully) reasonable assumption that this case was meant to belong to the category of \texttt{C1} contacts. The equivalence classes have been adjusted accordingly.

\subsubsection{Invalid Equivalence Classes}
\begin{tabular}{|p{.92\textwidth}|p{.03\textwidth}|}
  \hline
  {\bf Condition} & {\bf ID} \\
  \hline
    \texttt{your\_age < 0, others >= 0 $\implies$ INVALID} & 6 \\
  \hline
    \texttt{their\_age < 0, others >= 0 $\implies$ INVALID} & 7 \\
  \hline
    \texttt{time < 0, others >= 0 $\implies$ INVALID} & 8 \\
  \hline
    \texttt{distance < 0, others >= 0 $\implies$ INVALID} & 9 \\
  \hline
\end{tabular}

\newpage

\subsection{Boundary Value Testing (2 points)}

Use \emph{Boundary Value Testing} to derive a test-suite for
the function {\tt triage}. Specify the inputs points 
for {\tt classify}. Indicate clearly which equivalence
classes each test-case covers by referring to the numbers from
task (a). You can receive up to 2 points ($\frac{1}{2}$ a point per
test-case), where redundant test-cases and test-cases that do not
represent boundary values do not count.\\[1ex]

\begin{tabular}{|p{.61\textwidth}|p{.10\textwidth}|p{.10\textwidth}|}
  \hline
      {\bf Input} & {\bf Output } & {\bf Classes Covered}\\
          \hline
            \texttt{your\_age = 0 $\land$ their\_age = 11 $\land$ time = 15 $\land$ distance = 1m} & \texttt{C1} & 1 \\
          \hline
            \texttt{your\_age = 0 $\land$ their\_age = INT\_MAX $\land$ time = INT\_MAX $\land$ distance = 0} & \texttt{C1} & 1 \\
          \hline
            \texttt{your\_age = 0 $\land$ their\_age = 0 $\land$ time = 15 $\land$ distance = 1m} & \texttt{C2} & 2 \\
          \hline
            \texttt{your\_age = 9 $\land$ their\_age = 9 $\land$ time = INT\_MAX $\land$ distance = 0} & \texttt{C2} & 2 \\
          \hline
            \texttt{your\_age = 0 $\land$ their\_age = 0 $\land$ time = 14 $\land$ distance = 2} & \texttt{NEITHER} & 3, 4 \\
          \hline
            \texttt{your\_age = 0 $\land$ their\_age = 0 $\land$ time = INT\_MAX $\land$ distance = 0} & \texttt{NEITHER} & 3, 4 \\
          \hline
            \texttt{your\_age = -1 $\land$ their\_age = 0 $\land$ time = 0 $\land$ distance = 0} & \texttt{INVALID} & 6 \\
          \hline
            \texttt{your\_age = 0 $\land$ their\_age = -1 $\land$ time = 0 $\land$ distance = 0} & \texttt{INVALID} & 7 \\
          \hline
            \texttt{your\_age = 0 $\land$ their\_age = 0 $\land$ time = -1 $\land$ distance = 0} & \texttt{INVALID} & 8 \\
          \hline
            \texttt{your\_age = 0 $\land$ their\_age = 0 $\land$ time = 0 $\land$ distance = -1} & \texttt{INVALID} & 9 \\
          \hline
    \end{tabular}

\newpage

\section{Invariants (5 points)}

\noindent
Consider the following program, where {\tt t}, {\tt x}, {\tt y}, and {\tt z}
are integer values in $\mathbb{Z}$ (that means no over- or underflow
can happen):
\begin{lstlisting}[language=C,basicstyle=\ttfamily\normalsize]
  z = 1;
  if (x > y) {
    int t = x; x = y; y = t;
  }
  while (y > x) {
    x = x + 1;
    y = y - 1;
    z = z + (y - x);
  }
\end{lstlisting}

Consider the formulas below; tick the correct box
($\Box\,\!\!\!\!\!\!\checkmark$) to indicate 
whether they are loop invariants for the program above.
\begin{itemize}
  \item If the formula is an inductive invariant for the loop, provide an
    informal argument that the invariant is inductive.
  \item If the formula $P$ is an invariant that is \emph{not} inductive,
    give values of {\tt x} and {\tt y} before and after the loop
    body demonstrating that the Hoare triple 
    \begin{displaymath}
    \{ P \wedge B \}\quad {\tt x = x + 1;\;y = y - 1;\;z = z + (y - x)}\quad \{ P \}
    \end{displaymath}
    (where $B$ is {\tt(y > x)}) does not hold. This means that you need to find
    a starting state in which $P \wedge B$ evaluates to true and which results in
    a violation of $P$ after executing the loop body.
\item Otherwise,
  provide values of {\tt x} and {\tt y} that correspond to
  a reachable state showing that the formula is \emph{not} an 
  invariant.
\end{itemize}

\noindent
\begin{tabular}
  {|p{.19\textwidth}p{.25\textwidth}p{.26\textwidth}p{.11\textwidth}|}
\hline
$(x\leq y)$
 & $\Box$ Inductive Invariant & $\Box$ Non-inductive Inv. &
$\boxtimes$ Neither\\[1ex]
Justification: &&& \\
\hline
\multicolumn{4}{l}{It is not even non-inductive, and this can be shown by beginning with our supposed} \\
\multicolumn{4}{l}{invariant at the end of the loop, and hoisting it over several times: $y \geq x \mapsto y - 1 \geq x \mapsto$} \\
\multicolumn{4}{l}{$y - 1 \geq x + 1 \mapsto y \geq x + 2$. For instance $x = 2 \land y = 1$ as an initial state would violate $B$.} \\
[1cm]
\hline
$(x-y)\leq 1$ 
& $\boxtimes$ Inductive Invariant & $\Box$ Non-inductive Inv. &
$\Box$ Neither\\[1ex]
Justification: &&&\\
\hline
\multicolumn{4}{l}{This one is inductive, by similar reasoning as before: $(x - y) \leq 1 \mapsto(x - (y - 1)) \leq 1 \mapsto$} \\
\multicolumn{4}{l}{$(x + 1 - (y - 1)) \leq 1 \mapsto x + 1 - y + 1 \leq 1 \implies x + 1 \leq y$. In fact, $P$ in this case is just} \\
\multicolumn{4}{l}{another way to write $B$, so this definition is inductive.} \\
[1cm]
\hline
$(y - x)+2 \neq 0$ & $\boxtimes$ Inductive Invariant & $\Box$ Non-inductive Inv. &
$\Box$ Neither\\[1ex] 
Justification: &&&\\
\hline
\multicolumn{4}{l}{Doing the same steps: $(y - x) + 2 \not = 0 \mapsto (y - 1 - x) + 2 \not = 0 \mapsto (y - 1 - (x + 1)) + 2 \not = 0 \mapsto$} \\
\multicolumn{4}{l}{$y - x \not = 0 \implies y \not = x$. This means that $P$ as hoisted above the statements follows directly} \\
\multicolumn{4}{l}{from $B$.} \\
[1cm]
\hline
$z \geq 0$ & $\Box$ Inductive Invariant & $\boxtimes$ Non-inductive Inv. &
$\Box$ Neither\\[1ex] 
Justification: &&&\\
\hline
\multicolumn{4}{l}{Doing the same steps: $z \geq 0 \mapsto z + (y - x) \geq 0 \mapsto z + (y - 1 - x) \geq 0 \mapsto$} \\
\multicolumn{4}{l}{$z + (y - 1 - (x + 1)) \geq 0 \mapsto z + y \geq x + 2$. It now depends what the value of $z$ is in the} \\
\multicolumn{4}{l}{environment, but since an inductive invariant requires that the invariant still holds without} \\
\multicolumn{4}{l}{this knowledge, this is a non-inductive invariant. An example would be} \\
\multicolumn{4}{l}{$x = 1 \land y = 0 \land z = 0$.} \\
[1cm]
\hline
$z \geq 1$ & $\Box$ Inductive Invariant & $\Box$ Non-inductive Inv. &
$\boxtimes$ Neither\\[1ex] 
Justification: &&&\\
\hline
\multicolumn{4}{l}{This is the same as the previous one, but with the difference that we aren't covered in the} \\
\multicolumn{4}{l}{case the difference at line $z = z + (y - x)$ evaluates to $z = z - 1$. An example configuration} \\
\multicolumn{4}{l}{would be that of the previous example, $x = 1 \land y = 0 \land z = 0$.} \\
\multicolumn{4}{l}{} \\
\end{tabular}

\end{document}
}
